T:Type, R:(TT), P:(T).
(x, y:T. Dec(R(x,y)))
 (x:T. Dec(P(x)))
 (y:T. L:T List. (x:T. (R(x,y))  (x  L)))
 WellFnd{i}(T;x,y.R(x,y))
 (y:T. Dec(x:T. (R^+(x,y) & P(x)))) 

latex

Definitions	type List, (x  l), x,y. t(x;y), WellFnd{i}(A;x,y.R(x;y)), x. t(x), {T}, x.A(x), P  Q, x:AB(x), Dec(P), P & Q, , R^+, Type, x(s), f(a), x:A. B(x), t  T, x:A. B(x), x:A  B(x), (xL.P(x)), P  Q, left + right, False, a < b, s = t, A, Void, A c B, x:A.B(x), x f y, Trans(T;x,y.E(x;y)), l[i], , {x:A| B(x)} , , A  B, ||as||, #$n, , rel_exp(T;R;n)
Lemmas	nat plus inc, rel exp wf, nat plus wf, select wf, length wf1, nat wf, rel plus implies, rel plus trans, not wf, rel-rel-plus, decidable l exists better-extract, decidable and, decidable cand, decidable l exists, decidable wf, rel plus wf, wellfounded wf, l member wf